m, n:. (m  n) = (m * n)   

latex

Up	groups 1
Definitions of Statement	|g|, *, e, IMonoid, Mon, AbMon, OCMon, <,+>
Definitions	t  T, x:A. B(x), False, A, A  B, P  Q, t.1, P & Q, |g|, IMonoid, P  Q, P  Q, <,+>, , t.2, e, , *, x f y, , Mon, AbMon, OCMon
Lemmas	nat wf, le wf, ocmon wf, grp id wf, grp op wf, grp car wf, monoid p wf, nat add mon wf2, mon nat op zero, mon nat op unroll, mul bounds 1a